A:Type, eq:EqDecider(A), B:(AType), P:(A), f:x:A fp B(x), a:A.
(a  dom(f))
 (b:A. ((P(b)))  (b = a))
 (fpf-vals(eq;P;f) = [<a, f(a)>]  ((x:A  B(x)) List)) 

latex

Definitions

a:A fp B(a), let x = a in b(x), fpf-vals(eq;P;f), t  T, x:A. B(x), EqDecider(T), , x(s), x. t(x), Top, x  dom(f), b, , P  Q, P  Q, remove-repeats(eq;L), no_repeats(T;l), (x  l), P & Q, P  Q, filter(P;l), deq-member(eq;x;L), if b then t else f fi , P  Q, A, b, Unit, False, {T}, SQType(T), S  T, ||as||, i  j , hd(l), A  B, tl(l), i <z j, i z j, nth_tl(n;as), l[i], Y, , f(x), map(f;as), zip(as;bs)

Lemmas

ge wf, tl wf, hd wf, non neg length, length wf1, member wf, bool cases, bool sq, remove-repeats wf, nil member, false wf, cons member, no repeats wf, no repeats cons, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, deq-member wf, bnot wf, not wf, l member wf, assert-deq-member, remove-repeats property, iff wf, assert wf, fpf-dom wf, fpf-trivial-subtype-top, fpf wf, bool wf, deq wf